(declare-fun str6 () String)
(declare-fun str7 () String)
(declare-fun str8 () String)
(assert (str.contains str6 (str.++ str8 str8)))
(assert (= str8 "AvGYCNjngoF"))
(push)
(assert (not (= str7 (str.++ "pQHRoRXwvFIzQiVZFnTiewbePvXHRuMcpJcoKPmTTjPAvGYCNjngoFlOKzthoecQkHVgJxtfUnssQkHhSMKmIYSbwvtzRUFAQ" str8 str8))))
(push)
(pop)
(assert (str.contains (str.replace_re_all str7 (str.to_re str8) (str.++ "pQHRoRXwvFIzQiVZFnTiewbePvXHRuMcpJcoKPmTTjPAvGYCNjngoFlOKzthoecQkHVgJxtfUnssQkHhSMKmIYSbwvtzRUFAQ" str6)) (str.replace_re str8 (str.to_re str7) str8)))
(check-sat)
